基于SPIN的系统建模研究

doi:10.3969/j.issn.1006-2475.2012.09.055

计算机与现代化 ›› 2012, Vol. 1 ›› Issue (9): 209-214.doi: 10.3969/j.issn.1006-2475.2012.09.055

基于SPIN的系统建模研究

徐小丽

北京航空航天大学计算机学院,北京100191

收稿日期:2012-05-21 修回日期:1900-01-01 出版日期:2012-09-21 发布日期:2012-09-21

School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

XU Xiao-li

School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

Received:2012-05-21 Revised:1900-01-01 Online:2012-09-21 Published:2012-09-21

摘要/Abstract

摘要： 模型检测由于其自动化程度高，是形式化验证领域最受欢迎的验证方式之一。要使用模型检测器，首先要对要验证的系统进行建模。本文阐述模型检测技术的基本原理，并采用SPIN模型检测器对Promela建模进行研究。最后给出一个简单的公交车运行模型，并对实验结果进行分析。


关键词: 模型检测, 建模, SPIN, Promela

Abstract: Because of the high degree of automation, model checking technology has become one of the most popular way to ensure correctness in the formal verification field. To use the model checker, the user should model the verification-needed system. This paper summarizes the basic principles of model checking technology and explores the Promela modeling with model checker SPIN. Finally, a simple bus operation prototype model is given, and the experimental results are analyzed.


Key words: model checking, modeling, SPIN, Promela

徐小丽. 基于SPIN的系统建模研究[J]. 计算机与现代化, 2012, 1(9): 209-214.

XU Xiao-li. School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China[J]. Computer and Modernization, 2012, 1(9): 209-214.

[1]	杜康, 郭鲁钰, 徐啟蕾, 单宝明, 张方坤. 基于模型种群分析变量选择的红外光谱建模方法[J]. 计算机与现代化, 2023, 0(12): 48-52.
[2]	管金平, 杨晋吉, 杨成龙. 基于概率模型的Raft协议形式化验证[J]. 计算机与现代化, 2023, 0(09): 77-81.
[3]	史清林, 刘丽哲, 李行健. 基于大规模MIMO的散射信道估计技术[J]. 计算机与现代化, 2022, 0(12): 18-25.
[4]	丁绪东, 杨东润, 刘慧, 赵星凯, 张迎, 孙梅, . 数据驱动的蒸发器在线建模方法[J]. 计算机与现代化, 2022, 0(11): 22-31.
[5]	刘慧, 丁绪东, 杨东润, 张迎, 刘忠晨, 孙梅. 一种太阳能集热系统集热量实时预测的混合建模方法[J]. 计算机与现代化, 2022, 0(10): 55-61.
[6]	曾旭阳, 孙卡. 基于DI-Guy的校园消防训练仿真[J]. 计算机与现代化, 2021, 0(08): 35-39.
[7]	江超群, 童晶, 郭明灯, 陆荣杰, 陈正鸣. 基于三周期极小曲面的三维打印全接触鞋垫建模方法[J]. 计算机与现代化, 2021, 0(05): 13-19.
[8]	宋鑫, 樊志强, . 基于Laguerre 前向神经网络的信息服务性能建模方法 [J]. 计算机与现代化, 2021, 0(03): 1-6.
[9]	刘宏飞, 杨耀权, 杨雨航. 基于改进光流特征的运动目标跟踪[J]. 计算机与现代化, 2021, 0(03): 115-121.
[10]	刘梦超, 王玉玫, 吴亚非, 臧义华, 梁佳. 基于本体的军事装备知识建模及分析[J]. 计算机与现代化, 2021, 0(01): 76-80.
[11]	文晶，郑扬飞. 基于Stacking的社区矫正人员标签生成[J]. 计算机与现代化, 2020, 0(03): 60-.
[12]	陈艳琳，李志华，谢雪涵. 基于神经网络逆控制的水轮机调节系统[J]. 计算机与现代化, 2020, 0(01): 6-.
[13]	叶茜1,王玉斐2,傅毅3,唐玉兰1 . 基于GQM模型的工业控制系统风险评估方法[J]. 计算机与现代化, 2019, 0(08): 92-.
[14]	熊永芳,林友芳,武志昊. 带层次网络结构的业务系统层次组织结构发现[J]. 计算机与现代化, 2019, 0(07): 88-.
[15]	韩丽丽,王奇志,杨永刚. 机械臂抓取行为规划研究综述[J]. 计算机与现代化, 2018, 0(09): 11-.

基于SPIN的系统建模研究

School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价